The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic logic (...) without any structural rules, as our basic framework. Residuated lattices are the algebraic structures corresponding to FL. In this setting, we introduce a criterion, called the propagation property, that can be stated both in syntactic and algebraic terminologies. We then show that, for any set R of structural rules, the cut elimination theorem holds for FL enriched with R if and only if R satisfies the propagation property. As an application, we show that any set R of structural rules can be "completed" into another set R*, so that the cut elimination theorem holds for FL enriched with R*, while the provability remains the same. (shrink)

Two constructions for adding an involution operator to residuated ordered monoids are investigated. One preserves integrality and the mingle axiom x 2x but fails to preserve the contraction property xx 2. The other has the opposite preservation properties. Both constructions preserve commutativity as well as existent nonempty meets and joins and self-dual order properties. Used in conjunction with either construction, a result of R.T. Brady can be seen to show that the equational theory of commutative distributive residuated lattices (without involution) (...) is decidable, settling a question implicitly posed by P. Jipsen and C. Tsinakis. The corresponding logical result is the (theorem-) decidability of the negation-free axioms and rules of the logic RW, formulated with fusion and the Ackermann constant t. This completes a result of S. Giambrone whose proof relied on the absence of t. (shrink)

Very few attempts have been made to survey patient opinions, particularly regarding the use of residual biospecimens and health information in research, to clarify their values. We conducted a questionnaire survey that targeted outpatients of a university hospital to gauge their awareness levels and understand patient perspectives on research that uses these items. Few patients felt that obtaining individual consent for each research study was necessary. Most patients expressed the view that researchers should be obligated to inform them about the (...) research use of their items and be subject to self-directed rules. The research community should try to obtain “societal consent regarding an opt-out system” from the public. A salient value-sharing-based governance structure is necessary for obtaining public trust. (shrink)

A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices.

A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices.

Structural completeness properties are investigated for a range of popular t-norm based fuzzy logics—including Łukasiewicz Logic, Gödel Logic, Product Logic, and Hájek's Basic Logic—and their fragments. General methods are defined and used to establish these properties or exhibit their failure, solving a number of open problems.

This article argues in general support of the sIRB rule, but also draws on recent empirical research to highlight several residual weaknesses in the US regulatory structure for research ethics review, and suggests ways in which these weaknesses might be addressed in future regulatory reforms to improve upon the sIRB rule.

Natural deduction with alternatives extends Gentzen–Prawitz-style natural deduction with a single structural addition: negatively signed assumptions, called alternatives. It is a mildly bilateralist, single-conclusion natural deduction proof system in which the connective rules are unmodi_ed from the usual Prawitz introduction and elimination rules — the extension is purely structural. This framework is general: it can be used for (1) classical logic, (2) relevant logic without distribution, (3) affine logic, and (4) linear logic, keeping the connective (...) class='Hi'>rules fixed, and varying purely structural rules. The key result of this paper is that the two principles that introduce kinds of irrelevance to natural deduction proofs: (a) the rule of explosion (from a contradiction, anything follows); and (b) the structural rule of vacuous discharge; are shown to be two sides of a single coin, in the same way that they correspond to the structural rule of weakening in the sequent calculus. The paper also includes a discussion of assumption classes, and how they can play a role in treating additive connectives in substructural natural deduction. (shrink)

Performing an inference involves irreducibly dynamic cognitive procedures. The article proposes that a non-associative information frame, corresponding to a residuated pogroupoid, underpins the information structure involved. The argument proceeds by expounding the informational turn in logic, before outlining the cognitive actions at work in deductive inference. The structural rules of Weakening, Contraction, Commutation, and Association are rejected on the grounds that they cause us to lose track of the information flow in inferential procedures. By taking the operation of (...) information application as the primary operation, the fusion connective is retained, with commutative failure generating a double implication. The other connectives are rejected. (shrink)

Atocha Aliseda gives in Abductive Reasoning (2006) a structural characterization of the forward explanatory reasoning from a theory to observational data. This paper discusses the converse problem of giving structural rules for the backward abductive reasoning from observations to explanatory theories.

We study structural rules in the context of multi-valued logics with finitely-many truth-values. We first extend Gentzen’s traditional structural rules to a multi-valued logic context; in addition, we propos some novel structural rules, fitting only multi-valued logics. Then, we propose a novel definition, namely, structural rules completeness of a collection of structural rules, requiring derivability of the restriction of consequence to atomic formulas by structural rules only. The restriction (...) to atomic formulas relieves the need to concern logical rules in the derivation. (shrink)

Atocha Aliseda’s Abductive Reasoning (2006) gives a structural characterization of the “forward” explana-tory reasoning from a theory to observational data. This paper asks whether there are any interesting structural rules for the “backward” abductive reasoning from observations to explanatory theories. Ignoring statistical cases, a partial explication of abduction is converse deductive explanation: h is abducible from e iff h deductively explains e. This relation of abducibility trivially satisfies Converse Entailment (if h entails e, then h is abducible (...) from e ), but it does not generally satisfy Converse Consequence (if h is abducible from e and g entails h, then g is abducible from e ), since deductive explanation is not always transitive. (shrink)

The dominant image of courts as agencies of trial and judgment has a long history in the common law world. Yet across that region sponsorship of settlement is now widely identified as the courts’ primary responsibility, transforming them into sites where the profoundly different rationalities that ground negotiated agreement increasingly supersede those of rule-based adjudication. This study examines the work of one English court—the Mayor's and City of London Court—in sponsoring settlement and considers how that role is legitimated on both (...) propositional and symbolic levels. This evolving role raises questions about the Victorian court premises themselves. How are we to regard the now frequently empty courtrooms, designed for trial and judgment and decorated with Gothic elevations linking them symbolically with processes of medieval kingship? Should we simply see this Victorian site of contemporary settlement processes as no more than the quaint residue of a vanished era? Or can these historic features retain potency and relevance at a symbolic level, providing legitimacy for bilateral negotiation rather than the open processes of trial and judgment for which they were originally constructed? (shrink)

In recent years, substructural approaches to paradoxes have become quite popular. But whatever restrictions on structural rules we may want to enforce, it is highly desirable that such restrictions be accompanied by independent philosophical motivation, not directly related to paradoxes. Indeed, while these recent developments have shed new light on a number of issues pertaining to paradoxes, it seems that we now have even more open questions than before, in particular two very pressing ones: what (independent) motivations do (...) we have (if any) for restrictions on structural rules, and what to make of the plurality of new logics emerging from these restrictions, i.e. how to ‘choose’ among the different options. In this paper, we address these two questions from the perspective of a dialogical conception of logic that we've been advocating in recent years. We will argue that dialogical interpretations of structural rules, that is, as rules determining specific properties of the dialogues in question, provide a conveniently neutral framework to adjudicate between the different substructural proposals that have been made in the literature on paradoxes. (shrink)

In our previous paper [5], we have studied Kripke-type semantics for propositional logics without the contraction rule. In this paper, we will extend our argument to predicate logics without the structure rules. Similarly to the propositional case, we can not carry out Henkin's construction in the predicate case. Besides, there exists a difficulty that the rules of inference () and () are not always valid in our semantics. So, we have to introduce a notion of normal models.

Different natural deduction proof systems for intuitionistic and classical logic —and related logical systems—differ in fundamental properties while sharing significant family resemblances. These differences become quite stark when it comes to the structural rules of contraction and weakening. In this paper, I show how Gentzen and Jaśkowski’s natural deduction systems differ in fine structure. I also motivate directed proof nets as another natural deduction system which shares some of the design features of Genzen and Jaśkowski’s systems, but which (...) differs again in its treatment of the structural rules, and has a range of virtues absent from traditional natural deduction systems. (shrink)

We show that if the structural rules are admissible over a set \ of atomic rules, then they are admissible in the sequent calculus obtained by adding the rules in \ to the multisuccedent minimal and intuitionistic \ calculi as well as to the classical one. Two applications to pure logic and to the sequent calculus with equality are presented.

According to semantic antirealism, intuitionistic logic satisfies the requirement that truth should be constrained by provability in principle. Some philosophers have argued that semantic antirealism must be committed to effective provability and that the commitment leads to a stronger kind of logical revisionism exemplified by substructural logics. I shall take into account two different kinds of reply. The first is concerned with meaning per se and grasp or fixing of meaning. It rests on the idea that if we have a (...) method which may be used over some surveyable range, we have determined a way of applying the method everywhere in principle, and that this is enough as far as fixing or grasping meaning is concerned. The second concerns two radical antirealist principles disqualifying structural rules: Token Preservation and Preservation of Local Feasibility. Against criticisms, I shall argue that conceptual support may be provided for both. The main point in this debate is that there is a decisive difference between the rejection of classical logic via the curbing of the epistemic idealizations embedded in structural rules and the rejection of classical logic via the intuitionistic criticism of invalid introduction and elimination rules. It will be explained why the second rejection is stronger than the former. (shrink)

The contraction-free sequent calculus G4 for intuitionistic logic is extended by rules following a general rule-scheme for nonlogical axioms. Admissibility of structural rules for these extensions is proved in a direct way by induction on derivations. This method permits the representation of various applied logics as complete, contraction- and cut-free sequent calculus systems with some restrictions on the nature of the derivations. As specific examples, intuitionistic theories of apartness and order are treated.

The goal of the paper is to develop a universal semantic approach to derivable rules of propositional multiple-conclusion sequent calculi with structural rules, which explicitly involve not only atomic formulas, treated as metavariables for formulas, but also formula set variables, upon the basis of the conception of model introduced in :27–37, 2001). One of the main results of the paper is that any regular sequent calculus with structural rules has such class of sequent models that (...) a rule is derivable in the calculus iff it is sound with respect to each model of the semantics. We then show how semantics of admissible rules of such calculi can be found with using a method of free models. Next, our universal approach is applied to sequent calculi for many-valued logics with equality determinant. Finally, we exemplify this application by studying sequent calculi for some of such logics. (shrink)

We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.

The logical formalism of abductive reasoning is still an open discussion and various theories have been presented about it. Abduction is a type of non-monotonic and defeasible reasonings, and the logic containing such a reasoning is one of the types of non-nonmonotonic and defeasible logics, such as inductive logic. Abduction is a kind of natural reasoning and it is a solution to the problems having this form "the phenomenon of φ cannot be explained by the theory of Θ" and we (...) need to search for (or to adduce) an explanation for φ. Taking α as the explanation and <Θ,φ> as the abductive problem, Θ∪{α}⊨φ is the logical format of a strong abductive reasoning. In this article, the proof theory for first-order abductive calculus is proposed based on Gentzen-type first-order proof theory. Considering its dual, i.e., the semantic tableaux, and without the need to translate the formulas, this calculation is sound and complete. After examining the structural rules of this calculus, some metalogical considerations and open problems such as consistency, completeness and undecidability of this account have been addressed. (shrink)

This paper shows a role of the contraction rule in decision problems for the logics weaker than the intuitionistic logic that are obtained by deleting some or all of structural rules. It is well-known that for such a predicate logic L, if L does not have the contraction rule then it is decidable. In this paper, it will be shown first that the predicate logic FLec with the contraction and exchange rules, but without the weakening rule, is (...) undecidable while the propositional fragment of FLec is decidable. On the other hand, it will be remarked that logics without the contraction rule are still decidable, if our language contains function symbols. (shrink)

Gentzen’s classical sequent calculus has explicit structural rules for contraction and weakening. They can be absorbed by replacing the axiom P,¬P by Γ,P,¬P for any context Γ, and replacing the original disjunction rule with Γ,A,B implies Γ,AB.This paper presents a classical sequent calculus which is also free of contraction and weakening, but more symmetrically: both contraction and weakening are absorbed into conjunction, leaving the axiom rule intact. It uses a blended conjunction rule, combining the standard context-sharing and context-splitting (...) rules: Γ,Δ,A and Γ,Σ,B implies Γ,Δ,Σ,AB. We refer to this system as minimal sequent calculus.We prove a minimality theorem for the propositional fragment : any propositional sequent calculus S is complete if and only if S contains. Thus one can view as a minimal complete core of Gentzen’s. (shrink)

In this paper, we propose a game semantics for the (associative) Lambek calculus . Compared to the implicational fragment of intuitionistic propositional calculus, the semantics deals with two features of the logic: absence of structural rules, as well as directionality of implication. We investigate the impact of these variations of the logic on its game semantics.

As far as logic is concerned, the conclusion of Michael Dummett's manifestability argument is that intuitionistic logic, as first developed by Heyting, satisfies the semantic requirements of antirealism. The argument may be roughly sketched as follows: since we cannot manifest a grasp of possibly justification-transcendent truth conditions, we must countenance conditions which are such that, at least in principle and by the very nature of the case, we are able to recognize that they are satisfied whenever they are. Intuitionistic logic (...) satisfies the semantic requirement that we should either eschew the notion of truth altogether and replace it by provability in principle, or constrain it by provability in principle (Dummett [1973] 1978). (Handout: 1-5). Some philosophers have argued that the traditional antirealist desideratum of decidability in principle is too weak, so that semantic antirealism properly construed must be committed to effective decidability. As such, it either leads to strict finitism (Wright [1982] 1993) [Handout: 6] or to a much stronger kind of logical revisionism than the one considered by intuitionists (whether or not they accept the manifestability argument): substructural logics, and in particular linear logics, rather than intuitionistic logic, satisfy the semantic requirements of strict antirealism (Dubucs and Marion 2004) [Handout: 8-9]. I shall develop two different kinds of replies. The first is concerned with the notion of meaning per se and looks to strict finitism directly, although not on the ground that it would provide a correct way of dealing with Soritic-type paradoxes (the original and primary focus of discussion in Wright [1982] 1993). The second is concerned with the justification of structural and logical rules in a natural deduction system à la Gentzen. It will deal in particular with the criticism of the structural rules of Weakening and Contraction [Handout: 10 and 11]. The first kind of reply, which Dummett has partially taken into consideration, is that if we jettison the effectively vs. in principle distinction, as applied to manifestability-type arguments, we end up with an unsatisfactory explanation of how the meaning of statements covering the practically unsurveyable or pro tempora undecided cases is fixed. The idea is that if we have a method which may be used over some small range, we have determined a way of applying the method everywhere in principle and that this is enough as far as fixing meaning is concerned. Decidability in principle is just what we need with respect to manifestation of grasp of meaning. In this perspective, antirealism shouldn't be strict and manifestability-type arguments need not be applied as far as the strict finitist would want to [Handout: 7]. It follows that there is no reason to think that practical feasibility should be built in assertibility conditions and proofs be construed dynamically as acts in the strict antirealist's acception of that term [Handout: 8]. I shall then look at one radical antirealist principle disqualifying structural rules, namely Token Preservation, arguing against Bonnay and Cozic's criticisms of Dubucs and Marion (Bonnay and Cozic 3 2007) that some conceptual support may be provided for Token Preservation, which doesn't rely on a causal misreading of the turnstile [Handout: 13, 14]. I shall then assess the merits and limits of radical antirealism and the logic of feasible proofs with respect to the original Dummettian argument in favour of semantic antirealism (provided it has indeed revisionist implications for logic), whether the radical antirealist merely stipulates what human feasibility amounts to, or dispenses with structural rules in order to argue in favour of a curb on the epistemic idealizations they unwarrantedly embed. It will be noted here that there is a great difference, conceptually speaking, between the rejection of classical logic via the curbing of the epistemic idealizations embedded in structural rules, and the rejection of classical logic via the criticism of the introduction and elimination rules which fix the meaning of the classical constants. The kind of logical revisionism envisaged by intuitionists from Heyting on is in many respects stronger than the one envisaged by advocates of linear logic, should they ground their arguments on an endorsement of strict antirealism. The crucial case of excluded middle is telling. Because of the splitting of the constants in linear logic (Handout: 12], two distinct laws of excluded middle may be formulated (Handout: 15), but the traditional arguments of Brouwer and Heyting against the classical law yield a stronger revision than the substructural revision with its admission of these two (very) weak versions of the law. (Project: a clearer conception is needed of how the introduction and elimination rules for the logical connectives in the intuitionistic calculus depend on the structural rules which the radical antirealist wishes to reject.). (shrink)

Some empirical evidence in the artificial language acquisition literature has been taken to suggest that statistical learning mechanisms are insufficient for extracting structural information from an artificial language. According to the more than one mechanism (MOM) hypothesis, at least two mechanisms are required in order to acquire language from speech: (a) a statistical mechanism for speech segmentation; and (b) an additional rule-following mechanism in order to induce grammatical regularities. In this article, we present a set of neural network studies (...) demonstrating that a single statistical mechanism can mimic the apparent discovery of structural regularities, beyond the segmentation of speech. We argue that our results undermine one argument for the MOM hypothesis. (shrink)

This provocative book outlines a powerful and original theory of liberty structured by the liberal conception of justice and the rule of law. Drawing on insights from philosophy, political theory, economics, and law, he shows how this new conception of liberty can confront, and solve, the central societal problems of knowledge, interest, and power.

The variety of residuated lattices includes a vast proportion of the classes of algebras that are relevant for algebraic logic, e.g., \-groups, Heyting algebras, MV-algebras, or De Morgan monoids. Among the outliers, one counts orthomodular lattices and other varieties of quantum algebras. We suggest a common framework—pointed left-residuated \-groupoids—where residuated structures and quantum structures can all be accommodated. We investigate the lattice of subvarieties of pointed left-residuated \-groupoids, their ideals, and develop a theory of left nuclei. Finally, we extend some (...) parts of the theory of join-completions of residuated \-groupoids to the left-residuated case, giving a new proof of MacLaren’s theorem for orthomodular lattices. (shrink)

Written with verve and intensity (and a good bit of wordplay), this is the long-awaited study of Flaubert and the modern literary field that constitutes the ...

The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the (...) structural rules. Next, Hubert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.The first part of the paper, which follows, contains the first two sections, which deal with sequent-systems and Hubert-formulations. The second part, due to appear in the next issue of this journal, will contain the third section, which deals with groupoid models. (shrink)

The purpose of this paper is to connect the proof theory and the model theory of a family of prepositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related to BCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in (...) the structural rules. Next, Hilbert-style formulations are given for these logics, and algebraic completeness results are demonstrated with respect to residuated lattice-ordered groupoids. Finally, model structures related to relevant model structures (of Urquhart, Fine, Routley, Meyer, and Maksimova) are given for our logics. These model structures are based on groupoids parallel to the sequent-systems. This paper lays the ground for a kind of correspondence theory for axioms of logics with implication weaker than Heyting's, a correspondence theory analogous to the correspondence theory for modal axioms of normal modal logics.Below is the sequel to the first part of the paper, which appeared in the previous issue of this journal (vol. 47 (1988), pp. 353–386). The first part contained sections on sequent-systems and Hilbert-formulations, and here is the third section on groupoid models. This second part is meant to be read in conjunction with the first part. (shrink)

We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show (...) that the logic associated with and is algebraizable, with the variety of residuated lattice-ordered groupoids with unit serving as its equivalent algebraic semantics. Overcoming technical complications arising from the lack of associativity, we introduce a generalized version of a logical matrix and apply the method of quasicompletions to obtain an algebra and a quasiembedding from the matrix to the algebra. By applying the general result to specific cases, we obtain important logical and algebraic properties, including the cut elimination of and various extensions, the strong separation of , and the finite generation of the variety of residuated lattice-ordered groupoids with unit. (shrink)

In this paper, we will develop an algebraic study of substructural propositional logics over FLew, i.e. the logic which is obtained from intuitionistic logics by eliminating the contraction rule. Our main technical tool is to use residuated lattices as the algebraic semantics for them. This enables us to study different kinds of nonclassical logics, including intermediate logics, BCK-logics, Lukasiewicz’s many-valued logics and fuzzy logics, within a uniform framework.

In an article dating back in 1992, Kosta Došen initiated a project of modal translations in substructural logics, aiming at generalising the well-known Gödel–McKinsey–Tarski translation of intuitionistic logic into S4. Došen's translation worked well for (variants of) BCI and stronger systems (BCW, BCK), but not for systems below BCI. Dropping structural rules results in logic systems without distribution. In this article, we show, via translation, that every substructural (indeed, every non-distributive) logic is a fragment of a corresponding sorted, (...) residuated (multi) modal logic. At the conceptual and philosophical level, the translation provides a classical interpretation of the meaning of the logical operators of various non-distributive propositional calculi. Technically, it allows for an effortless transfer of results, such as compactness and the Löwenheim-Skolem property and it opens up new directions for deducing properties of substructural logic systems by establishing appropriate transfer theorems. (shrink)

We study filters in residuated structures that are associated with congruence relations (which we call -filters), and develop a semantical theory for general substructural logics based on the notion of primeness for those filters. We first generalize Stone’s sheaf representation theorem to general substructural logics and then define the primeness of -filters as being “points” (or stalkers) of the space, the spectrum, on which the representing sheaf is defined. Prime FL-filters will turn out to coincide with truth sets under various (...) well known semantics for certain substructural logics. We also investigate which structural rules are needed to interpret each connective in terms of prime -filters in the same way as in Kripke or Routley-Meyer semantics. We may consider that the set of the structural rules that each connective needs in this sense reflects the difficulty of giving the meaning of the connective. A surprising discovery is that connectives , ⅋ of linear logic are linearly ordered in terms of the difficulty in this sense. (shrink)